#!/bin/bash

# Inputs
INPUT_FILE=$1

# Outputs
OUTPUTS_DIRECTORY=outputs
TIME_RESULTS_FILE=$OUTPUTS_DIRECTORY"/"$INPUT_FILE".results_minisat"

# Executables
MINISAT="/home/jaime/Dropbox/Mestrado/Pesquisa/Ursa/sat_solvers/minisat/core/minisat"

HEADER=`cat $INPUT_FILE | grep "p cnf"`

VARIABLES=`echo $HEADER | cut -d " " -f 3`
CLAUSES=`echo $HEADER | cut -d " " -f 4`


if [[ "$#" != 1 ]]
then
	echo "Wrong number of parameters. Expected 1." >&2
	exit 1
fi

if ! [[ -e "$MINISAT" ]]
then
	echo "Could not find the solver." >&2
	exit 1
fi

echo "File = $INPUT_FILE" >> $TIME_RESULTS_FILE
echo "Formula has $VARIABLES variables and $CLAUSES clauses" >> $TIME_RESULTS_FILE

/usr/bin/time -o $TIME_RESULTS_FILE -a $MINISAT $INPUT_FILE >> $TIME_RESULTS_FILE
echo >> $TIME_RESULTS_FILE
